googologywikiaorg-20200223-history
User blog:Nayuta Ito/Is this bigger than Rayo's number?
This number is from a Japanese googology competition held (technically) a month ago. I am just translating other person's number, so my translation might be wrong. According to the original author, it's bigger than BIG FOOT. Number: The alphabets of a formal language FOL is defined as followings: \mathrm{FOL_{constant}}:=\{2n+1|n\in\mathbb{N}\} \mathrm{FOL_{variable}}:=\{2(2n+1)|n\in\mathbb{N}\} For a natural number a , \mathrm{FOL_{a,\ argument\ function}}:=\{4(2^{a+1}(2n+1)+1)|n\in\mathbb{N}\} For a natural number a , \mathrm{FOL_{a,\ argument\ relation}}:=\{8(2^{a+1}(2n+1)+1)|n\in\mathbb{N}\} \mathrm{FOL_{logical}}:=\{16,48,80\} \mathrm{FOL_{contradiction}}:=\{32\} \mathrm{FOL_{logical\ formula}}:=\{64(2n+1)|n\in\mathbb{N}\} And the syntax is as follows: # A term in FOL is a string in FOL which is an element of \mathrm{FOL_{constant}} ; an element of \mathrm{FOL_{variable}} ; or f(t_1,t_2,\cdots,t_a) , where a is a natural number, f is an element of \mathrm{FOL_{a,\ argument\ function}} , and t_1,t_2,\cdots t_n are terms. # A logical formula in FOL is a string in FOL which is an element of \mathrm{FOL_{logical\ formula}} ; 32; 16x(P) where x is an element of \mathrm{FOL_{variable}} ; (P)48(Q) where P and Q are formulae; 80(P) where P is a formula; or f(t_1,t_2,\cdots,t_a) , where a is a natural number, f is an element of \mathrm{FOL_{a,\ argument\ relation}} , and t_1,t_2,\cdots t_n are terms. # A logical formula in FOL is first-order if and only if it does not contain an element of \mathrm{FOL_{logical\ formula}} in its string. Especially, the formal language FOL', FOL without \mathrm{FOL_{logical\ formula}} , is a formal language of first-order predicate logic, and the following is a logical formula A_{ZFC} in FOL: ZFC axioms combined by AND operator in FOL. For a logical formula A and first-order logical formula P in FOL, P is provable from the axiom A means P is provable in FOL' using (finite first-order logical formula obtained by replacing all elements of \mathrm{FOL_{logical\ formula}} into some concrete first-order logical formulae in A) as an axiom. For a logical formula A in FOL, A is consistent means that 32 is not provable from the axiom A. For a natural number n, a Peano arithmetic term tn is defined as follows: *If n=0, tn is 0 (as a constant). *If n>0, tn is S(tn-1) (as a term). For a natural number n, the natural number f(n) is defined as follows: The smallest minimum number bigger than any natural number m such that: There exists a logical formula A and first-order logical formula P in FOL, both of which have n or less symbols, such that: A connotes Peano arithmetic; Con(A_ZFC) implies Con(A), where Con means consistent; there exists only one element of \mathrm{FOL_{variable}} (call it x) such that it's not bounded by 16; and m is the smallest natural number where 80(Q) is not provable with A, where Q is: P, whose all x without bound by 16 are replaced by t. the image of tm in A, and 16x((P)48(x=t)) combined by AND operator in FOL. A bit "better" explanation: For a natural number n, the natural number f(n) is defined as follows: First, take a natural number m ,a first-order logical formula P and a logical formula A in FOL(both P and A must have n or less symbols). However, A must satisfy these conditions: A connotes Peano arithmetic; Con(A_ZFC) implies Con(A), where Con means consistent; there exists only one element of \mathrm{FOL_{variable}} (call it x) such that it's not bounded by 16. Now take P and replace all x without bound by 16 are into t, the image of tm in A. Combine P and 16x((P)48(x=t)) by AND operator in FOL and call it Q. Whether 80(Q) is provable with A or not depends on m, A, and P. If you take m big enough, 80(Q) is always not provable with A no matter what P is. There exists the mininum of such number m, so take it and add 1. That's the f(n). "fight for not being able to write the smallest proof" number is defined as f(10^100). Category:Blog posts